perm filename FRAME.AX[W81,JMC] blob sn#562992 filedate 1981-02-12 generic text, type C, neo UTF8
COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	axiom frame:
C00005 ENDMK
C⊗;
axiom frame:

	∀x a e s.(assigns(e,x,a,s) ⊃ value(x,result(e,s)) = a)
	∀y e s.unchanged(y,e,s) ⊃ value(y, result(e,s)) = value(y,s))

;;

axiom walk:
	∀p z s.assigns(does(p,walk(z)),location(p),z,s)
	∀p z s.assigns(does(p,walk(z)),tiredness(p),value(tiredness(p),s)+1,s)
	∀x p z s.(¬(x=p) ⊃ unchanged(location(x),does(p,walk(z)),s))
;;

These axioms involve further reification.  Here  x  is a "basic entity".
The intent is that an event  e  may be described as assigning new values to
certain basic entities and leaving others unchanged.  value(x,s) is the
value of the entity  x  in the situation s.  As an example, location(I)
would be a basic entity in a re-axiomatization of the airport problem, and
we would have

	value(location(I),S0) = at(desk).

In our new formulation  result(e,s)  is the situation that results
when the event   e   occurs in the situation  s.  An action is a kind
of event, and the action that interests us here is  does(p, walk(z)),
e.g.  does(I, walk(car)).  One of the effects of an action can be
an assignment to a basic entity, and our sentence

	assigns(does(p,walk(z)),location(p),z,s)

asserts that the event  does(p,walk(z))  assigns   z  to  location(p).

	We threw in the axiom that  tiredness(p)  increases by  1  when
a person walks somewhere to illustrate that this formalism permits the
ready addition of more effects of an action.  Of course, we still must
explicitly axiomatize what remains unchanged in order to be sure that
preconditions for subsequent actions are preserved.